library IEEE;
use IEEE.STD_LOGIC_1164.ALL;
use IEEE.STD_LOGIC_ARITH.ALL;
use IEEE.STD_LOGIC_UNSIGNED.ALL;
entity formula is
    port(
        enable: in std_logic;
        reset: in std_logic;
        a: in std_logic_vector(0 to 7);
        satisfied: out std_logic
    );
end entity formula;
architecture formula_behavior of formula is
signal sat_temp: std_logic;

--loop breaking signals
signal clause_signal: std_logic;

type clause is array(0 to 7) of std_logic_vector(0 to 1);
type formula is array(0 to 31)of clause;

signal temp_clause: clause;
signal clause_literal: std_logic_vector(0 to 1);
signal a_value : std_logic;

signal f: formula;



begin  --architecture
	
f(0) <= ("00","11","01","11","00","00","00","00");
f(1) <= ("00","00","01","00","00","01","00","11");
f(2) <= ("00","00","01","01","00","00","01","00");
f(3) <= ("00","01","00","00","00","00","11","11");
f(4) <= ("00","00","01","00","01","00","00","01");
f(5) <= ("00","00","11","00","11","00","01","00");
f(6) <=	("00","11","00","11","00","00","01","00");
f(7) <= ("01","00","00","00","01","00","00","11");
f(8) <= ("01","00","01","00","00","00","00","11");
f(9) <= ("11","11","00","00","00","00","01","00");
f(10) <= ("11","00","00","00","11","11","00","00");
f(11) <= ("00","00","11","00","11","00","01","00");
f(12) <= ("00","00","00","01","01","00","01","00");
f(13) <= ("00","01","01","11","00","00","00","00");
f(14) <= ("00","11","11","00","00","00","00","01");
f(15) <= ("01","00","00","01","00","01","00","00");
f(16) <= ("11","11","11","00","00","00","00","00");
f(17) <= ("11","11","00","00","00","00","11","00");
f(18) <= ("11","00","00","00","00","01","00","01");
f(19) <= ("00","00","11","11","00","00","00","01");
f(20) <= ("00","00","00","01","11","11","00","00");
f(21) <= ("00","00","01","11","00","01","00","00");
f(22) <= ("11","01","01","00","00","00","00","00");
f(23) <= ("01","11","00","00","00","00","11","00");
f(24) <= ("00","00","00","11","00","11","00","11");
f(25) <= ("00","11","01","00","00","00","01","00");
f(26) <= ("11","11","00","00","00","01","00","00");
f(27) <= ("11","00","01","11","00","00","00","00");
f(28) <= ("01","00","00","11","00","00","00","11");
f(29) <= ("00","00","11","01","00","00","00","01");
f(30) <= ("00","00","00","11","01","11","00","00");
f(31) <= ("00","00","00","11","01","11","00","00");

--solver process
process(enable, reset, a)
begin --process
	
if reset = '1' then
	
	sat_temp <= '0';

else
	
	if enable = '1' then

		clause_signal <= '0';
		for i in 0 to 31 loop
			clause_signal <= '1';			
			temp_clause <= f(i);

			
			for j in 0 to 7 loop
			
				clause_literal <= temp_clause(j);
				a_value <= a(j);
				
				if clause_literal = "01" then
					if a_value = '1' then
						clause_signal <= '1';
					end if;
					
				elsif clause_literal = "11" then
					if a_value = '0' then
						clause_signal <= '1';

					end if;		
				end if;
	
			end loop;
			
			if clause_signal = '0' then
				sat_temp <= '0';
			else
				sat_temp <= sat_temp;				
			end if;			   
			
		end loop;

		if clause_signal = '1' then
			sat_temp <= '1';
		else
			sat_temp <= '0';
		end if;
	end if;
end if;	

end process;

--output switching process
process(sat_temp)

begin --process
satisfied <= sat_temp;
end process;

end architecture formula_behavior;